Inference at * 1 1 1 1 1 1 
Iof proof for Lemma ax choice:



1. A : Type
2. B : Type
3. Q : AB
4. g : x:Ay:B  Q(x,y)
5. x : A
6. y1 : B
7. y2 : Q(x,y1)
8. <y1, y2> = g(x)
  Q(x,<y1, y2>.1) 

latex

 by ((AbReduce 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t.1